From bceffd5d394a1d7eb536302d4a92321edb4e473e Mon Sep 17 00:00:00 2001 From: DanieCuevas <43822444+DanielCuevas1208@users.noreply.github.com> Date: Mon, 3 Aug 2026 18:29:09 -0700 Subject: [PATCH] feat: extend gatework --- .github/workflows/ci.yml | 4 +- CHANGELOG.md | 16 ++++ README.md | 34 +++++++-- app/Main.hs | 62 +++++++++------ fixtures/adder.golden.vcd | 2 +- fixtures/assert.golden.vcd | 2 +- fixtures/bus.golden.vcd | 2 +- fixtures/counter.golden.vcd | 2 +- fixtures/gates.golden.vcd | 2 +- fixtures/haddader.golden.vcd | 2 +- fixtures/hcounter.golden.vcd | 2 +- fixtures/libadder.golden.vcd | 2 +- fixtures/reg2.golden.vcd | 2 +- fixtures/register.golden.vcd | 2 +- fixtures/reset.golden.vcd | 2 +- fixtures/shared.golden.vcd | 2 +- fixtures/tristate.golden.vcd | 2 +- fixtures/unknown.golden.vcd | 2 +- gatework.cabal | 3 +- src/Gatework/Netlist.hs | 56 ++++++++++++-- test/Spec.hs | 142 +++++++++++++++++++++++++++++++++++ 21 files changed, 295 insertions(+), 50 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3be5a57..d9277e5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -80,8 +80,8 @@ jobs: run: cabal run gatework -- --netlist fixtures/unknown.net --duration 8 --output /tmp/unknown.vcd --set d=1 --at 4 d=0 - name: Compare the undefined demo with the golden file run: diff fixtures/unknown.golden.vcd /tmp/unknown.vcd - - name: Run the bus demo - run: cabal run gatework -- --netlist fixtures/bus.net --duration 3 --output /tmp/bus.vcd --set 'a[0]=1,a[2]=1,b[1]=1,b[3]=1' + - name: Run the bus demo with whole-bus values + run: cabal run gatework -- --netlist fixtures/bus.net --duration 3 --output /tmp/bus.vcd --set a=0101,b=1010 - name: Compare the bus demo with the golden file run: diff fixtures/bus.golden.vcd /tmp/bus.vcd - name: Run the shared bus demo diff --git a/CHANGELOG.md b/CHANGELOG.md index a63884f..acb85f5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,22 @@ All notable changes to Gatework appear in this file. The format follows the Keep a Changelog convention. This project uses semantic versioning. +## [0.11.0.0] - 2026-08-03 + +### Added + +- Set a whole input bus on the command line with one bit string. +- Accept whole-bus bit strings in the --set and --at options. +- The bit string lists the most-significant bit first. +- The value may use 0, 1, x, and z. +- Reject a value that does not match the bus width. +- Add deterministic tests and a QuickCheck property for whole-bus values. +- Run the bus demo with whole-bus values in the CI workflow. + +### Changed + +- Bump the package version to 0.11.0.0. + ## [0.10.0.0] - 2026-08-03 ### Added diff --git a/README.md b/README.md index 9ce0bd3..826acc0 100644 --- a/README.md +++ b/README.md @@ -44,6 +44,7 @@ You can do these tasks: - Pass a bus through a module port. - Sample a whole bus into a register on one clock edge. - Check a single bus bit with an assertion. +- Set a whole bus on the command line with one bit string. ## Architecture @@ -469,7 +470,7 @@ The `NOT` gate shows the unknown until the flip-flop samples data. Run four-bit bus operations with gates and a register. ```powershell -cabal run gatework -- --netlist fixtures/bus.net --duration 3 --output bus.vcd --set 'a[0]=1,a[2]=1,b[1]=1,b[3]=1' +cabal run gatework -- --netlist fixtures/bus.net --duration 3 --output bus.vcd --set a=0101,b=1010 ``` The command writes this output: @@ -481,6 +482,11 @@ Duration: 3 time units Assertions: 7 passed ``` +The value `a=0101` sets the whole input bus `a`. +The string lists bits from the most-significant bit down. +So `a[3]=0`, `a[2]=1`, `a[1]=0`, and `a[0]=1`. +This command gives the same waveform as per-bit assignments. + The inputs `a` and `b` are four-bit buses. The gate `XOR combine` applies bitwise across both buses. The module `invert_bus` passes the bus `x` through a four-bit port. @@ -799,6 +805,23 @@ assert s[0] = 1 at 0 assert s[2] = 0 at 4 ``` +### Whole-bus input values + +The command line sets one bit or a whole bus. + +```text +--set a[0]=1 +--set a=0101 +--at 2 b=1010 +``` + +A bit assignment names one signal. +The value must be 0, 1, x, or z. +A bus assignment names the bus without brackets. +The value must match the bus width. +The bit string lists the most-significant bit first. +The value may use 0, 1, x, and z. + ### Modules and instances A module is a reusable subcircuit. @@ -885,6 +908,7 @@ Deterministic tests also cover bus declarations, bitwise gates, bit references, Deterministic tests also cover multi-driver resolution, scheduled driver changes, flip-flop output exclusivity, the shared-bus fixture, and its golden output. Deterministic tests also cover module library loading, cross-library module references, duplicate module names, and library file validation. Deterministic tests also cover the report command, its header order, its counter table, and its golden output. +Deterministic tests also cover whole-bus input values, their bit order, their error cases, scheduled whole-bus transitions, and their golden output. QuickCheck properties cover gate algebra, full adder correctness, scheduled input sampling, reset sampling, register width, and assertion soundness. QuickCheck properties also compare the hierarchical adder and counter with their flat versions. QuickCheck properties also cover the four-state model and the tri-state buffer truth table. @@ -892,6 +916,7 @@ QuickCheck properties also compare a bus circuit with a bitwise reference model. QuickCheck properties also compare the shared bus with a per-time resolution model. QuickCheck properties also compare a library adder with its flat version. QuickCheck properties also compare the counter report with the simulated waveform. +QuickCheck properties also compare whole-bus input values with per-bit reference values. QuickCheck runs one hundred random cases for each property. The gate properties cover the complete truth table. @@ -919,6 +944,7 @@ Golden tests compare the counter, register, reset, two-bit register, assertion, The golden report test compares the counter report table with its golden file. CI runs every demo and compares its output with the golden file. CI runs the report demo and compares it with the report golden file. +CI runs the bus demo with whole-bus input values. CI confirms that a missing library file stops the run. ## Limitations @@ -952,8 +978,6 @@ A bus expands into single-bit signals, so the VCD stays flat. A flip-flop bus output must have a `wire` or `output` declaration. A reference to a whole bus uses the declared width. An assertion addresses one bit, not a whole bus. -Input assignments on the command line address one bit. -The CLI does not accept whole-bus values. One module declaration cannot live inside another. An instance output must connect to a declared signal. The dotted instance names are part of the VCD signal names. @@ -963,6 +987,7 @@ The report prints every signal in the stable signal order. ## Roadmap +Release 0.11.0.0 completed whole-bus input values on the command line. Release 0.10.0.0 completed the waveform report command. Release 0.9.0.0 completed module libraries. Release 0.8.0.0 completed multi-driver wire resolution. @@ -975,8 +1000,7 @@ Release 0.2.0.0 completed scheduled input transitions. Remaining work: -1. Add whole-bus input values on the command line. -2. Add multi-bit values in the VCD timeline. +1. Add multi-bit values in the VCD timeline. ## License diff --git a/app/Main.hs b/app/Main.hs index a7e02f7..790ef41 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,8 +1,13 @@ module Main (main) where import Data.List (intercalate) -import Gatework.Logic (Logic, logicChar, parseLogic) -import Gatework.Netlist (netlistSignals, parseNetlistFileWithLibraries) +import Gatework.Logic (Logic, logicChar) +import Gatework.Netlist + ( Netlist + , netlistSignals + , parseNetlistFileWithLibraries + , resolveInputAssignments + ) import Gatework.Report (renderReport) import Gatework.Simulator ( AssertionFailure (..) @@ -23,8 +28,8 @@ data Options = Options , optionDuration :: Integer , optionOutput :: FilePath , optionOutputExplicit :: Bool - , optionInputs :: [(String, Logic)] - , optionScheduled :: [(Time, String, Logic)] + , optionInputs :: [(String, String)] + , optionScheduled :: [(Time, String, String)] , optionLibraries :: [FilePath] } @@ -55,17 +60,23 @@ run command = do case parsed of Left message -> failWith message Right netlist -> - case simulateWithScheduledInputs netlist (optionInputs options) (optionScheduled options) (optionDuration options) of + case resolveInputAssignments netlist (optionInputs options) of Left message -> failWith message - Right simulation -> do - wroteFile <- emit command simulation - let summaryHandle = if wroteFile then stdout else stderr - if wroteFile - then putStrLn ("Wrote " ++ optionOutput options) - else pure () - hPutStrLn summaryHandle ("Signals: " ++ show (length (netlistSignals netlist))) - hPutStrLn summaryHandle ("Duration: " ++ show (optionDuration options) ++ " time units") - reportAssertions summaryHandle simulation + Right inputOverrides -> + case resolveScheduledAssignments netlist (optionScheduled options) of + Left message -> failWith message + Right scheduled -> + case simulateWithScheduledInputs netlist inputOverrides scheduled (optionDuration options) of + Left message -> failWith message + Right simulation -> do + wroteFile <- emit command simulation + let summaryHandle = if wroteFile then stdout else stderr + if wroteFile + then putStrLn ("Wrote " ++ optionOutput options) + else pure () + hPutStrLn summaryHandle ("Signals: " ++ show (length (netlistSignals netlist))) + hPutStrLn summaryHandle ("Duration: " ++ show (optionDuration options) ++ " time units") + reportAssertions summaryHandle simulation commandOptions :: Command -> Options commandOptions (CommandRun options) = options @@ -129,14 +140,21 @@ parseOptions arguments = parseMore defaultOptions arguments parseMore options {optionScheduled = optionScheduled options ++ [(time, name, logic) | (name, logic) <- values]} rest option : _ -> Left ("unknown option: " ++ option) -parseAssignments :: String -> Either String [(String, Logic)] +parseAssignments :: String -> Either String [(String, String)] parseAssignments value = mapM parseAssignment (splitOn ',' value) where parseAssignment assignment = case break (== '=') assignment of - (name, '=' : rawLogic) | not (null name) -> case parseLogic rawLogic of - Just logic -> Right (name, logic) - Nothing -> Left ("input value must be 0, 1, x, or z: " ++ assignment) - _ -> Left ("input assignment must use signal=0, signal=1, signal=x, or signal=z: " ++ assignment) + (name, '=' : rawValue) | not (null name) && not (null rawValue) -> + Right (name, rawValue) + _ -> Left ("input assignment must use signal=value: " ++ assignment) + +resolveScheduledAssignments :: Netlist -> [(Time, String, String)] + -> Either String [(Time, String, Logic)] +resolveScheduledAssignments netlist = fmap concat . mapM step + where + step (time, name, value) = do + resolved <- resolveInputAssignments netlist [(name, value)] + pure [(time, signal, logic) | (signal, logic) <- resolved] splitOn :: Char -> String -> [String] splitOn delimiter value = case break (== delimiter) value of @@ -151,7 +169,7 @@ failWith message = do usage :: String usage = intercalate "\n" - [ "gatework [report] --netlist FILE [--library FILE] [--duration N] [--output FILE] [--set signal=0,signal=1,signal=x,signal=z] [--at TIME signal=0,signal=1,signal=x,signal=z]" + [ "gatework [report] --netlist FILE [--library FILE] [--duration N] [--output FILE] [--set signal=value] [--at TIME signal=value]" , "" , "Simulate a netlist and write a VCD waveform." , "Run 'gatework report' to write a text waveform table instead." @@ -159,6 +177,8 @@ usage = intercalate "\n" , "Use --library to load reusable module definitions from another file." , "Repeat --library to load more than one module file." , "Use --at to change input signals at a fixed time during the run." - , "Use x for an unknown value and z for a floating value." + , "A signal value is 0, 1, x, or z." + , "Set a whole bus with a bit string, for example --set a=0101." + , "The bit string lists the most-significant bit first." , "Check assert declarations in the netlist against the waveform." ] diff --git a/fixtures/adder.golden.vcd b/fixtures/adder.golden.vcd index 79330cf..9219d11 100644 --- a/fixtures/adder.golden.vcd +++ b/fixtures/adder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/assert.golden.vcd b/fixtures/assert.golden.vcd index f0ae630..f73e380 100644 --- a/fixtures/assert.golden.vcd +++ b/fixtures/assert.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $comment assert y = 1 at 0 diff --git a/fixtures/bus.golden.vcd b/fixtures/bus.golden.vcd index d2d4e3c..ed44583 100644 --- a/fixtures/bus.golden.vcd +++ b/fixtures/bus.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $comment assert x[0] = 1 at 0 diff --git a/fixtures/counter.golden.vcd b/fixtures/counter.golden.vcd index 00bc6c0..86ef1a4 100644 --- a/fixtures/counter.golden.vcd +++ b/fixtures/counter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/gates.golden.vcd b/fixtures/gates.golden.vcd index ea35367..a3c8098 100644 --- a/fixtures/gates.golden.vcd +++ b/fixtures/gates.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $comment assert nand_out = 1 at 0 diff --git a/fixtures/haddader.golden.vcd b/fixtures/haddader.golden.vcd index 96b4acd..e7240bd 100644 --- a/fixtures/haddader.golden.vcd +++ b/fixtures/haddader.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/hcounter.golden.vcd b/fixtures/hcounter.golden.vcd index 6a79210..1f021f2 100644 --- a/fixtures/hcounter.golden.vcd +++ b/fixtures/hcounter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/libadder.golden.vcd b/fixtures/libadder.golden.vcd index 96b4acd..e7240bd 100644 --- a/fixtures/libadder.golden.vcd +++ b/fixtures/libadder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reg2.golden.vcd b/fixtures/reg2.golden.vcd index 1730604..c6e140d 100644 --- a/fixtures/reg2.golden.vcd +++ b/fixtures/reg2.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/register.golden.vcd b/fixtures/register.golden.vcd index 8cf1130..de97888 100644 --- a/fixtures/register.golden.vcd +++ b/fixtures/register.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reset.golden.vcd b/fixtures/reset.golden.vcd index cca9050..1d95ec7 100644 --- a/fixtures/reset.golden.vcd +++ b/fixtures/reset.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/shared.golden.vcd b/fixtures/shared.golden.vcd index e4231cf..555e6dd 100644 --- a/fixtures/shared.golden.vcd +++ b/fixtures/shared.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/tristate.golden.vcd b/fixtures/tristate.golden.vcd index 417ae2e..ec75d1d 100644 --- a/fixtures/tristate.golden.vcd +++ b/fixtures/tristate.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/unknown.golden.vcd b/fixtures/unknown.golden.vcd index 621768a..c089ace 100644 --- a/fixtures/unknown.golden.vcd +++ b/fixtures/unknown.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.10.0.0 + gatework 0.11.0.0 $end $comment assert q = x at 0 diff --git a/gatework.cabal b/gatework.cabal index e11b398..61da6af 100644 --- a/gatework.cabal +++ b/gatework.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: gatework -version: 0.10.0.0 +version: 0.11.0.0 synopsis: Event-driven digital logic simulation in Haskell description: Gatework parses typed netlists, runs combinational gates and D @@ -13,6 +13,7 @@ description: circuits. A module library file stores reusable module definitions. The command-line tool loads libraries with the --library option. A waveform report command prints the signal values as a text table. + The command-line tool also sets a whole bus with one bit string. GTKWave and other waveform viewers can open the output. homepage: https://github.com/DanielCuevas1208/gatework bug-reports: https://github.com/DanielCuevas1208/gatework/issues diff --git a/src/Gatework/Netlist.hs b/src/Gatework/Netlist.hs index 4184530..fb6aa29 100644 --- a/src/Gatework/Netlist.hs +++ b/src/Gatework/Netlist.hs @@ -12,6 +12,7 @@ module Gatework.Netlist , parseNetlistFile , parseNetlistFileWithLibraries , parseNetlistWithLibraries + , resolveInputAssignments ) where import Control.Exception (IOException, try) @@ -79,6 +80,7 @@ data Netlist = Netlist , netlistGates :: [Gate] , netlistFlipFlops :: [DFlipFlop] , netlistAssertions :: [Assertion] + , netlistBusWidths :: [(String, Int)] } deriving (Eq, Show) @@ -127,10 +129,11 @@ data RawModule = RawModule data ParsedNetlist = ParsedNetlist { parsedModules :: Map String Module , parsedDeclarations :: [Declaration] + , parsedBusWidths :: Map String Int } emptyNetlist :: Netlist -emptyNetlist = Netlist [] [] [] [] [] [] [] +emptyNetlist = Netlist [] [] [] [] [] [] [] [] parseNetlistFile :: FilePath -> IO (Either String Netlist) parseNetlistFile = parseNetlistFileWithLibraries [] @@ -165,8 +168,9 @@ parseNetlistWithLibraries libraries source = do let signatureModules = signatureOnlyModules combinedModules modules <- mapM (resolveModule sources signatureModules) combinedModules validateModulesWithSources sources modules - declarations <- resolveTopLevel signatureModules rawDeclarations - netlist <- flattenParsed (ParsedNetlist modules declarations) + widths <- topLevelWidths rawDeclarations + declarations <- resolveTopLevel signatureModules widths rawDeclarations + netlist <- flattenParsed (ParsedNetlist modules declarations widths) _ <- validateNetlist netlist pure netlist @@ -474,9 +478,8 @@ moduleWidths raw = addWidth widths (RawClock clock) = insertWidth widths (clockSignal clock) 1 addWidth widths _ = Right widths -resolveTopLevel :: Map String Module -> [RawDeclaration] -> Either String [Declaration] -resolveTopLevel signatureModules rawDeclarations = do - widths <- topLevelWidths rawDeclarations +resolveTopLevel :: Map String Module -> Map String Int -> [RawDeclaration] -> Either String [Declaration] +resolveTopLevel signatureModules widths rawDeclarations = concat <$> mapM (resolveDeclaration signatureModules widths) rawDeclarations topLevelWidths :: [RawDeclaration] -> Either String (Map String Int) @@ -776,7 +779,8 @@ checkModuleFlipFlop moduleDef declared clockSignals flipFlop = do flattenParsed :: ParsedNetlist -> Either String Netlist flattenParsed parsed = do expanded <- concat <$> mapM (expandTop parsed) (parsedDeclarations parsed) - pure (foldl' addDeclaration emptyNetlist expanded) + let netlist = foldl' addDeclaration emptyNetlist expanded + pure netlist {netlistBusWidths = busWidthList (parsedBusWidths parsed)} expandTop :: ParsedNetlist -> Declaration -> Either String [Declaration] expandTop parsed declaration = case declaration of @@ -859,6 +863,44 @@ netlistSignals netlist = nub ++ map gateOutput (netlistGates netlist) ) +busWidthList :: Map String Int -> [(String, Int)] +busWidthList widths = + [(name, width) | (name, width) <- Map.toAscList widths, width > 1] + +resolveInputAssignments :: Netlist -> [(String, String)] -> Either String [(String, Logic)] +resolveInputAssignments netlist = fmap concat . mapM resolveOne + where + widths = Map.fromList (netlistBusWidths netlist) + inputs = netlistInputs netlist + resolveOne (name, value) + | Just width <- Map.lookup name widths = do + resolved <- expandBus name width value + unless (all ((`elem` inputs) . fst) resolved) $ + Left ("input override is not an input: " ++ name) + pure resolved + | otherwise = do + logic <- parseInputValue name value + pure [(name, logic)] + +expandBus :: String -> Int -> String -> Either String [(String, Logic)] +expandBus name width value + | length value /= width = + Left ( "bus " ++ name ++ " has width " ++ show width + ++ ", but the value has " ++ show (length value) ++ " bits" ) + | otherwise = sequence + [ case parseLogic [char] of + Just logic -> Right (bitAt name width index, logic) + Nothing -> + Left ("input value must be 0, 1, x, or z: " ++ name ++ "=" ++ value) + | (index, char) <- zip [width - 1, width - 2 .. 0] value + ] + +parseInputValue :: String -> String -> Either String Logic +parseInputValue name value = maybe + (Left ("input value must be 0, 1, x, or z: " ++ name ++ "=" ++ value)) + Right + (parseLogic value) + trim :: String -> String trim = dropWhile isSpace . reverse . dropWhile isSpace . reverse diff --git a/test/Spec.hs b/test/Spec.hs index d382bd6..fbbe4cd 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -15,6 +15,7 @@ import Gatework.Netlist , parseNetlist , parseNetlistFileWithLibraries , parseNetlistWithLibraries + , resolveInputAssignments ) import Gatework.Report (renderReport) import Gatework.Simulator @@ -264,6 +265,15 @@ main = do , testReportHeader , testReportCounterTable , testGoldenCounterReport + , testWholeBusAssignmentExpansion + , testWholeBusAssignmentFourState + , testWholeBusWidthMismatch + , testWholeBusInvalidCharacter + , testWholeBusBitReference + , testWholeBusNonInputRejected + , testWholeBusScalarValue + , testWholeBusScheduledRegister + , testWholeBusGoldenVCD ] properties <- forM [ ("AND is commutative", quickCheckResult propAndCommutative) @@ -309,6 +319,7 @@ main = do , ("shared bus follows the resolution model", quickCheckResult (propSharedBusResolution shared)) , ("library adder matches the flat adder", quickCheckResult (propLibraryAdderMatchesFlat adder libadder)) , ("counter report matches the waveform", quickCheckResult (propCounterReportMatchesWaveform counter)) + , ("whole-bus values match per-bit values", quickCheckResult propWholeBusMatchesBitwise) ] $ \(label, action) -> do result <- action @@ -1838,6 +1849,115 @@ testGoldenCounterReport = do pure (renderReport simulation) check "counter report matches golden file" (actual == Right golden) +wholeBusNetlist :: Either String Netlist +wholeBusNetlist = parseNetlist (unlines + [ "input a[4]" + , "output y[4]" + , "wire y[4]" + , "gate NOT inv (a) -> y" + ]) + +testWholeBusAssignmentExpansion :: IO Bool +testWholeBusAssignmentExpansion = case wholeBusNetlist of + Left _ -> check "whole-bus values expand most-significant bit first" False + Right netlist -> + check "whole-bus values expand most-significant bit first" $ + resolveInputAssignments netlist [("a", "0101")] + == Right + [ ("a[3]", Low) + , ("a[2]", High) + , ("a[1]", Low) + , ("a[0]", High) + ] + +testWholeBusAssignmentFourState :: IO Bool +testWholeBusAssignmentFourState = case wholeBusNetlist of + Left _ -> check "whole-bus values accept x and z" False + Right netlist -> + check "whole-bus values accept x and z" $ + resolveInputAssignments netlist [("a", "1z0x")] + == Right + [ ("a[3]", High) + , ("a[2]", TriState) + , ("a[1]", Low) + , ("a[0]", Undefined) + ] + +testWholeBusWidthMismatch :: IO Bool +testWholeBusWidthMismatch = case wholeBusNetlist of + Left _ -> check "whole-bus values reject a width mismatch" False + Right netlist -> + check "whole-bus values reject a width mismatch" $ + resolveInputAssignments netlist [("a", "01")] + == Left "bus a has width 4, but the value has 2 bits" + +testWholeBusInvalidCharacter :: IO Bool +testWholeBusInvalidCharacter = case wholeBusNetlist of + Left _ -> check "whole-bus values reject invalid characters" False + Right netlist -> + check "whole-bus values reject invalid characters" $ + resolveInputAssignments netlist [("a", "0a1b")] + == Left "input value must be 0, 1, x, or z: a=0a1b" + +testWholeBusBitReference :: IO Bool +testWholeBusBitReference = case wholeBusNetlist of + Left _ -> check "bit references still set one signal" False + Right netlist -> + check "bit references still set one signal" $ + resolveInputAssignments netlist [("a[0]", "1"), ("a[2]", "0")] + == Right [("a[0]", High), ("a[2]", Low)] + +testWholeBusNonInputRejected :: IO Bool +testWholeBusNonInputRejected = case wholeBusNetlist of + Left _ -> check "whole-bus values reject a non-input bus" False + Right netlist -> + check "whole-bus values reject a non-input bus" $ + resolveInputAssignments netlist [("y", "0101")] + == Left "input override is not an input: y" + +testWholeBusScalarValue :: IO Bool +testWholeBusScalarValue = case parseNetlist (unlines + [ "input a" + , "wire out" + , "gate NOT inv (a) -> out" + ]) of + Left _ -> check "scalar inputs keep single values" False + Right netlist -> + check "scalar inputs keep single values" $ + resolveInputAssignments netlist [("a", "1")] + == Right [("a", High)] + +testWholeBusScheduledRegister :: IO Bool +testWholeBusScheduledRegister = case parseNetlist (unlines + [ "input a[4]" + , "output q[4]" + , "clock clk period=2" + , "dff reg clock=clk d=a q=q init=0,0,0,0" + ]) of + Left _ -> check "scheduled whole-bus values sample each bit" False + Right netlist -> check "scheduled whole-bus values sample each bit" $ case + resolveInputAssignments netlist [("a", "0011")] of + Left _ -> False + Right resolved -> case + simulateWithScheduledInputs netlist [] [(2, name, logic) | (name, logic) <- resolved] 4 of + Right simulation -> + valueAt simulation "q[0]" 3 == High + && valueAt simulation "q[1]" 3 == High + && valueAt simulation "q[2]" 3 == Low + && valueAt simulation "q[3]" 3 == Low + Left _ -> False + +testWholeBusGoldenVCD :: IO Bool +testWholeBusGoldenVCD = do + source <- readFile "fixtures/bus.net" + golden <- readFile "fixtures/bus.golden.vcd" + let actual = do + netlist <- parseNetlist source + overrides <- resolveInputAssignments netlist [("a", "0101"), ("b", "1010")] + simulation <- simulateWithInputs netlist overrides 3 + pure (renderVCD simulation) + check "whole-bus VCD matches golden file" (actual == Right golden) + splitOn :: Char -> String -> [String] splitOn delimiter value = case break (== delimiter) value of (part, _ : rest) -> part : splitOn delimiter rest @@ -2146,6 +2266,24 @@ propCounterReportMatchesWaveform netlist = , (time, _) <- entries ] +propWholeBusMatchesBitwise :: Property +propWholeBusMatchesBitwise = + forAll (choose (0, 15)) $ \aValue -> + forAll (choose (0, 15)) $ \bValue -> + case busXorNetlist of + Left _ -> property False + Right netlist -> + case resolveInputAssignments netlist + [ ("a", bitsText 4 aValue), ("b", bitsText 4 bValue) ] of + Left _ -> property False + Right wholeBus -> + case ( simulateWithInputs netlist wholeBus 0 + , simulateWithInputs netlist (busInputs "a" aValue 4 ++ busInputs "b" bValue 4) 0 + ) of + (Right wholeSim, Right bitSim) -> + property (renderVCD wholeSim == renderVCD bitSim) + _ -> property False + propGatesFixture :: Netlist -> Property propGatesFixture netlist = forAll (elements [Low, High]) $ \a -> @@ -2393,6 +2531,10 @@ busInputs base value width = | index <- [0 .. width - 1] ] +bitsText :: Int -> Int -> String +bitsText width value = + [if bit index value == 1 then '1' else '0' | index <- [width - 1, width - 2 .. 0]] + busValueAt :: Simulation -> String -> Int -> Time -> Int busValueAt simulation base width time = sum